Nuprl Lemma : atom-free-es-vartype
0,22
postcript
pdf
es
:ES,
i
,
x
:Id. AtomFree(Type;vartype(
i
;
x
))
latex
Definitions
x
:
A
B
(
x
)
,
P
&
Q
,
ESAtomAxiom{i:l}(
T
;
V
)
,
vartype(
i
;
x
)
,
ES
,
t
T
,
x
:
A
B
(
x
)
,
Id
,
Type
,
AtomFree(
T
;
x
)
,
x
:
A
.
B
(
x
)
Lemmas
event
system
wf
origin
es:ES, i, x:Id. AtomFree(Type;vartype(i;x)) es:ES, i, x:Id. AtomFree(Type;vartype(i;x)) 
B(x)
T
B(x)x:A. B(x)